| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), ES, EState(T), a:A fp B(a), f(a), Id,  , strong-subtype(A;B), P   Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e',  ,  b, constant_function(f;A;B), SWellFounded(R(x;y)),  , pred!(e;e'),   x,y. t(x;y), Void,  x:A.B(x), Top, S  T, suptype(S; T), first(e),  A, <a, b>, pred(e), x.A(x), x. t(x), P & Q, chain_sys(Cmd), E, chain_config(), AbsInterface(A), e  X, P  Q, {x:A| B(x)} , E(X), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , X(e), csupdate?(x), tt, inr x , "$token", ff, inl x , Atom, False, True, update-antecedent{i:l}(es;Cmd;Sys;Config;u), X Y = 0,  x:A. B(x), (e < e'), a < b, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), (e <loc e'), let x = a in b(x), valid-sys(es;Config;Sys;e), cr-antecedent{i:l}(es;Config;Cmd;Sys;u), sys-antecedent(es;Sys), e c e', (x l), Sys(valid), ccsucc?(x), let x,y = A in B(x;y), t.1, prior(X), csinput?(x), b, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p  q, p q,  , Dec(P), b | a, a ~ b, a b, a <p b, a < b, A c B, xL. P(x), (xL.P(x)), y is f*(x), r < s, q-rel(r;x), Outcome, l_disjoint(T;l1;l2), e loc e' , e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), P Q, f**(e), sender(e), e(e1,e2].P(e), @e(x v), (last change to x before e), pred(e), lastchange(x;e), es-init(es;e), le(X),  T, SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f g |
| Lemmas | es-causl weakening, es-causl transitivity2, es-causle weakening, sq stable from decidable, es-prior-interface-val, es-causle-le, es-locl wf, es-le wf, es-causle weakening locl, es-le weakening eq, es-le-causle, is-sys-valid, update-antecedent-lemma1, es-interface-subtype rel, decidable or, decidable assert, chain sys-cases, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, csinput? wf, ifthenelse wf, es-prior-interface wf, es-causl wf, es-E-interface-subtype rel, sys-valid wf, sys-valid-subtype, es-causle wf, sys-antecedent wf, es-interface-disjoint wf, update-antecedent wf, es-interface-val wf, csupdate? wf, es-interface-val wf2, true wf, false wf, es-interface wf, es-E-interface wf, bfalse wf, btrue wf, es-is-interface wf, chain config wf, es-E wf, chain sys wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf |
u:({e:E(Sys)|